The present application claims the benefit of the filing date of European Patent Application EP 05 020 124.3, filed on Sep. 15, 2005, which is hereby incorporated by reference in its entirety.
The present invention generally relates to a procedure for determining the quality of a quantity of properties describing a machine. The machine of the type under consideration can be both software and hardware. Within the meaning of this application a machine is suitable to be described by means of properties. Such properties are generally known to the person skilled in the art of functional verification of digital circuits. An exemplary machine is thus a digital circuit.
When performing functional verification, an RTL-description of a circuit is verified as to whether it will function properly. The quality of the RTL-description after functional verification is decisive for the success of a circuit design project. Remaining errors are likely to cause high costs, loss of time and reputation.
In addition, using simulation as the principal work horse in functional verification is standard. For this, input patterns are preset, either automatically or by the user, and the output patterns generated by simulation compared with expectations. Errors are detected if an output pattern does not meet with expectations. Automatic mechanisms for error detection in simulation are hereinafter called monitors.
In order to detect an error, there must be given a suitable input pattern for which the simulation produces an output pattern in which the error shows up. Even in small circuits the quantity of all possible input patterns is very large. In addition, the factor between the run time in the real circuit and its simulation is in the range of 106. Therefore only a few input patterns can be simulated in comparison with the total number, so that many functional errors remain undetected.
Increasingly so-called property checkers are used for functional verification. Property checkers are given, as something input something called a “property”, i.e. a relationship concerning certain aspects of the circuit, that is described in a formal language. Within surprisingly short time, the property checker yields a result in the form of                either the information that the property has been proven by the property checker. In this case the relationship between the behavior aspects which is described in the property will always occur, irrespective of how the circuit is operated        a rebuttal in which an input pattern for the circuit is described that violates the relationship between the behaviour aspects. This rebuttal is generated by the property checker.The automatic generation of counter-examples and the rapid checking of the property for all possible input patterns constitute a considerable advancement in the functional verification vis-à-vis simulation.        
For this reason, property checkers are also being implemented today by innovative verification groups. However, they only verify selectively as behavioural associations that are considered critical, which were chosen by a verification engineer based on his/her intuition and experience. This nonetheless only enables gradual improvements in the quality of the RTL description after verification. A relatively high number of errors in the design are still present in the result.
In the area of circuit verification by means of simulation, suggestions have already been made concerning procedures for the evaluation of the quality of the verification environment, which even calculate measures, which are supposed to be related to this quality. In this sense, the number and coverage of the input patterns used for simulation is, on the one hand, of the greatest importance for the quality of the verification environment and, on the other hand, the effort to achieve a multiplicity of different types of input patterns is also cause for a large resource requirement.
The corresponding procedures have already been in use for years and are supported by commercial EDG tools (see e.g. D. Dempster, M. Stuart: “Verification Methodology Manual—Techniques for Verifying HDL Designs”, Teamwork International, 2nd edition, 2001; and S. Tarisan, K. Keutzer: “Coverage Metrics for Functional Validation of Hardware Designs”, IEEE Design & Test of Computers. 2001.) The metrics for determining the measures are often code-based such as the line coverage, path coverage, assignment coverage and coverage of states for explicit state machines from the RTL code.
Such methods for measuring the quality of a verification were first developed for software verification. Unlike sequential software, however, hardware operates in the form of parallel processes. The dependencies generated by this are therefore not taken into account by the methods, so that the resulting quality measures are not reliable. Therefore, alternative measures have been suggested, for example those based on signals and require, for example, the assignment of all possible values. In addition, there are functional metrics, which display how often a certain functionality has been executed.
An inherent weakness in all of these approaches exists, however, in that attaining a level of 100% is far from securing the entire verification of all functionality. On the one hand, these approaches already achieve 100% coverage even when not all functionality and consequently all possible error sources in the circuit tested have been injected; on the other hand, there is no systematic test which shows whether the verification environment is capable of actually identifying every error that shows up.
The property check is described in exemplary terms in: A. Biere, A. Cimatti, M. Fujita, Y. Zhu: “Symbolic Model Checking using SAT procedures instead of BDDs” Proc. of 36th Design Automation Conference, 1999.; and in: “Formale Verifikation für Nicht-Formalisten (Formal Verification for Non-Formalists)”, Bormann, J. and Spalinger, C: (2001), Informationstechnik und Technische Informatik, Vol. 43, Issue 1/2001, Oldenburg Verlag.
When performing the quality assurance of a verification environment based on the property check, the issue is not necessarily the multiplicity and diversity of the input patterns, since a property checker functions as if it were inspecting all input patterns. It is rather the integrity of the property set, that is, whether each error in the circuit is detected when proving at least one of the properties.
Papers in this field are documented, for example, in: Hojati, R.: “Determining Verification Coverage Using Circuit Properties” U.S. Pat. No. 6,594,804, granted Jul. 15, 2003; Hoskote, Kam, Ho, and Zhao: “Coverage Estimation for Symbolic Model Checking” Proc. of 36th Design Automation Conference, 1999; and in: Hoskote, Y. “Property Coverage in Formal Verification”, Patent WO200079421-A2. These approaches are all based on sequentially injecting errors in the circuit and then checking whether at least one of the properties is disproved by the property checker in the circuit that has been modified in this way. If each of the errors injected ends up being disproved, the quality of the property set will be designated as sufficiently high. Otherwise, a measure concerning the proportion of those injected errors will be determined which were detected by the property set.
With the known procedures, it is either injected as an error that signals are inverted in various achievable states or the gate, at whose output the signal to be covered is picked up, is changed on the net list.
These procedures are heuristic. There is no guarantee that errors other than those injected will be detected by the property set. In addition to the quantity of properties, the procedures also require the circuit description.
Task
Since so far the properties, as described above, have only been applied in a selective manner and based on experience, a need exists for a procedure, which can reliably specify the quality of a quantity of properties in a reproducible manner, particularly in the form of a measure which can then be brought into accordance with a target value by expanding or adjusting the volume.
Furthermore, a need exists for procedures for more reliable verification and the specification of circuits based on the reproducible quality of a quantity of properties.
Consequently, one object of the invention in question is to specify procedures which determine and utilize the quality of a quantity of properties describing a machine without having to resort to excessive use of resources or experience values.
The above tasks are fulfilled by the invention by means of the procedures of the independent claim, preferred exemplary embodiments constituting the subject matter of dependent claims. By means of determining the quality of a quantity of properties describing a machine it is possible to utilize the properties in a more efficient manner.
In particular, the invention suggests a method for determining the quality of a quantity of properties describing a machine, comprising the determination of the existence of at least one sub-set of interrelated properties (P0, P1, . . . Pn); and the verification as to whether, by the interaction of (P0, P1, . . . Pn), for at least one input pattern of the machine, the value of a given term Q(t) is unambiguously/uniquely determined at least at one point in time at which it is not unambiguously/uniquely determined by the observation of the individual properties, Q(t) being only dependent on values of input and output parameters at points in time relative to t.
Here, Q(t) can be specified by the user or drawn from a reference table such as the list of the output parameters for the machine.
Q(t) is assumed as unambiguously/uniquely determined a the quantity of properties in an input pattern at a point in time T if for two sequences of value, on the output and internal parameters which supplement the input pattern in such a way that all properties of the quantity on it are valid, the value of Q(T) on the one supplement is equal to the value of Q(T) on the other supplement.
It is typical for the property check that the individual properties do not clearly determine an output parameter and consequently no Q(t) value since the properties are often in the form for all t:                ((Condition 1 for values of internal parameters at the point in time t) and        (Condition for input values at the point in time t) and        (Condition for input values at the point in time t+1) and        (Condition for input values at the point in time t+2) and        . . . and        (Condition for input values at the point in time t+n))        =>        ((Output parameters have definite values at the point in time t) and        (Output parameters have definite values at the point in time t+1) and        . . . and        (Output parameters have definite values at the point in time t+n) and        (Condition 2 for internal parameters at the point in time t+n)For this, the symbol => stands for the logical implication. The property itself does not determine any output parameters clearly because the complements to an input pattern can always be selected such that they violate condition 1 and then the values of the output parameters are able to be selected entirely contrary to one another. This type of complements completes the property and shows that no output value has been unambiguously/uniquely determined. The output values would be unambiguously/uniquely determined for an input pattern by the above property, if it is combined with a reset property, which ensures that the assignment of the internal signals following the activation of the reset input fulfils condition 1.        
As such, the invention is based on checking whether individual properties, which are only utilized and considered on a singular basis pursuant to the state of the art, exist in relation to one another.
Using this basic concept, properties can be systematically identified and utilized and for example, can also form multiple series of properties, which constitute a statement independent of internal signals concerning the input/output behaviour of the machine over a longer period of time.
In accordance with a preferred exemplary embodiment, the interrelated properties form a series of properties, which starts with a property that describes the initialization behaviour of the machine and constitutes a statement concerning the input/output behaviour of the machine or also of a circuit over a longer period of time, whereupon this statement is no longer dependant on internal signals.
Those properties not considered in the formation of the series of properties are conveniently reported to the user. In this process, it is possible to adjust the volume of properties in an efficient way or to complete them since either the property in question has been reformulated or a predecessor and/or successor property is to be provided for it.
If the properties have the form Pi=forall t: Ai=>Zi(t) with implicatively associated Boolean expressions Ai and Zi, which depend on values from the input, output and internal parameters at points in time relative to t, it can be conveniently checked during the determination step whether a series of reference points in time T1, T2, . . . Tn exists, such that the property given by the chaining of the properties with respect to the reference points in timeE=for all t. (A0(t)=>Z0(t)) and((A0(t) and A1(T1))=>Z1(T1)) and((A0(t) and A1(T1) and A2(T2))=>Z2(T2)) and. . . and((A0(t) and A1(T1) and . . . and An(Tn))=>Zn(Tn))already describes the input/output behaviour such that at least one input pattern, in which E clearly describes the value of Q(t) at a minimum of one point in time.
The procedure corresponding to the section “Automatic determining of all redundant specifications” proves this and the previous claims: For a quantity of properties, it is automatically determined, which properties are allowed to follow one another and how the reference points in time are to be formed during for this. Through this process, a graph is determined, whose only source is the property concerning the initializing behavior of the machine and whose finite paths, which start in the reset property, form the quantities or series of interrelated properties, which claims 1 to 12 refer to. Temporal domains, based on which the output signal is unambiguously/uniquely defined insofar the property is part of a series starting with the reset property and for which the reference points in time are selected in accordance with the values calculated, are calculated for every property and every output signal. Based on these temporal domains, it can then also be decided as to for which point in time Q(t) is unambiguously/uniquely defined.
The quantities of input patterns are conveniently described, on which Q(t) is unambiguously/uniquely determined for at least one point in time for each one.
If the properties are given in the implicative form described above, the quantity of input patterns, on which Q(t) is unambiguously/uniquely determined for at least one point in time for each one, consists of the input patterns for each of which a value series of the internal and output parameters is given such that there is at least one point in time t, for which the following applies based on these value series A0(t) and Z0(t) and A1(T1) and Z1(T1) and . . . and An(Tn).
In general, the reference points in time are dependant on t and on values of the input parameters at points in time relative to t. It is beneficial, however, if the reference points in time are only dependant on t.
The interrelated properties are arranged preferentially in a sequential relation, whereupon the values based on the output and internal signals, which are able to fulfill Zi−1(t) for the suitable selection of the input pattern especially for i≠0, are also able to fulfill the Boolean expression Ai(t′) for a suitable input series and for a point in time t′. This condition is also utilized in the procedure corresponding to the section “Automatic determining of all redundant specifications”.
The condition is closely related to the condition that Ai(t) and Zi−1(t) except for temporal displacement contain syntactically equal partial expressions concerning output and internal parameters.
By means of a sequential relation, which ensures between the elements of a finite quantity of properties that a series of properties can always be extended, it is possible to also check time ranges on an input pattern of unlimited length and to make statements for which points in time Q(t) is unambiguously/uniquely defined. In particular, it can determined that Q(t) on an input pattern is unambiguously/uniquely determined for all points in time following the first point in time.
The procedure according to the section “Calculation of all redundant specifications” sets the foundation by setting a graph whose finite paths set all series of properties possible.
In order to be able to identify additional sub-quantities, the step of identifying the existence of at least one sub-quantity of interrelated properties is repeated. By means of this process, it is e.g. possible to determine all possible property chains based on the properties.
The check preferred is whether the output parameters of the machine are unambiguously/uniquely determined for all input patterns and for all output parameters of a machine and for all points in time following the first point in time. This claim is proven by the combination of the procedure from the section “Automatic determination of all redundant specifications” together with the procedure for determining the completeness of a set of properties that is revealed in this patent specification.
A value measurement is identified and issued on a preferential basis, which corresponds to the probability that the value of this output parameter is unambiguously/uniquely determined at this point in time by the property for any input pattern starting with the circuit for any point in time and for any output parameter. This claim is proven by the combination of the procedure from the section “Automatic determination of all redundant specifications” together with the procedure revealed in this patent specification that is used to calculate the measure of completeness.
The invention also proposes a procedure for the functional verification of digital circuits, in which the circuit is checked using a quantity of properties whose value was determined as described previously and corresponds to a defined designation. In terms of the defined designation, a set threshold value may be involved or a value specified by the user, for which the value is believed to be sufficient because e.g. a further improvement can only be achieved by means of a disproportionate extra amount of work. The value can be monitored during the successive development of the properties and inferences can be made regarding the work to be incurred based on the difference between the designated value and the actual value.
The invention also proposes a procedure for the specification of digital circuits, in which the specification is created, based on a quantity of properties whose value was determined as described previously and corresponds to a defined designation. The value can be monitored during the successive development of the properties and inferences can be made regarding the work to be incurred based on the difference between the designated value and the actual value.
The invention proposes a procedure for the simulative verification of digital circuits, in which monitors are utilized, whereupon the monitors represent machines and the quality of the monitors is determined using the value of a quantity of properties described for the monitor. This quantity of properties is determined as previously described. In this manner, the quality of the monitor can be systematically tracked.
Finally, the invention proposes a procedure for the simulative verification of digital circuits, in which the coverage is determined by monitors, which are acquired from the assumptions of a set of properties whose value was determined pursuant to a procedure of the claims 1 to 15 and which correspond to a defined designation. In this way, it can particularly be ensured that the coverage is derived from a complete set of properties, thereby expressing functional aspects on the one hand and on the other hand, covering the entire functionality of a module. This coverage therefore combines the suitability of the functional coverage with the breadth of the coverage of code-based coverage and is thereby particularly suited for the system simulation.
In summary, the invention therefore enables checking a quantity of properties in terms of whether they cover the entire function of the circuit to be checked rather than only covering critical behavioural associations on a punctual basis. If the properties have all been proven on the machine (e.g. software or circuit) by a property checker, only errors also existent in the properties remain uncovered. The main problem of the simulation that errors remain undetected because they do not occur in any of the output patterns generated is avoided. As a result, the quality, which has the RTL description after completion of the verification, increases. As such, the invention allows a circuit verification to be conducted exclusively using a property check for the first time.
The fact that the mechanisms for the detection of errors (that is, the monitors or properties) could themselves be flawed and conceal circuit errors as a result thereof is a characteristic of every functional verification. This problem also exists in the simulation, which is recorded therein that the monitors have not detected any errors although they occur in an output pattern. If that happens, the monitor responsible for this was either coded incompletely, that is, it fails to conduct any check at all in one of the situations generated by the simulation or the monitor actually expects an incorrect value.
It can be ensured in an invention-pursuant manner that the properties check this behaviour at any point in time. Incompleteness in the properties is therefore automatically identified. As a result, errors that would otherwise remain undetected due to the incompleteness of the verification environment are also avoided.
In this context, it should be noted that the invention is not limited, in terms of its use, to the vicinity of a property checker. It can also identify incompleteness in monitors. For this, the monitors must be generated from properties, which were appropriately checked. The generation of monitors from properties is familiar to professionals. Procedures for the quality assurance of monitors to date are only known in terms of code review and recycling up to now, which however is not comparable with the invention-pursuant approach.
The properties commonly describe the machine or circuit behaviour to a more abstract extent than the RTL description. They mostly describe the machine resp. circuit behaviour over several cycles such that the processes in a machine/a circuit are presented universally and closed. As a result, they provide the verification engineer with a larger overview than the RTL description such that additional errors in the properties are avoided. The invention checks whether a quantity of properties has the quality of a machine/circuit description at a greater level of abstraction.
With the state-of-the-art vis-à-vis the simulation, the analysis of certain conditions with the objective of analyzing the number and variety of the input patterns simulated and consequently the probability that the flawed machine/circuit components were indeed conducted (coverage) is to be evaluated. The conditions implemented for this are commonly oriented with the text of the machine/circuit description. In this case, conditions are being worked with, which are fulfilled by the completion of a line (or also only one part of the line) in the machine/circuit description. This approach has the advantage that these kind of conditions consider each component of the machine respectively circuit in a wide-reaching manner. It is, however, regarded as inadequate because it does not take the parallel design of machine/circuit components into consideration. As a result, the text-oriented conditions are supplemented by conditions, which are fulfilled in specific partial processes (functional coverage). Nowadays, these kinds of conditions are only defined on a punctual basis, where they are necessary according to the intuition and experience of the verification engineer. The invention allows the definition of a set of such conditions, which are each fulfilled, if individual properties describe the machine/circuit behaviour. Such a set of conditions considers on the one hand all machine/circuit components and on the other also their parallel design. No procedures are yet known, with which sets of conditions of comparable quality can be generated.
All this helps keep the number of errors remaining in a design at a much lower level following the completion of a verification that utilizes said invention than following a simulation-based verification. Through the efficiency of the property checker, such verification most often saves an incredible amount of work.
In so doing, the invention delivers a specific criterion for the completion of the verification using the property checker in a preferred manner. If a property set is complete or suffices for the target value, the verification will end, if this is not the case, then it must be continued. The procedures corresponding to the state-of-the-art are not familiar with such criteria. In this case, the verification will be continued until the time or financial budget has been consumed or until certain specifications have been fulfilled, which heuristically suggest that now the residual risk has dropped below a tolerable value.
The invention can also be applied even before a set of properties has been verified with a property checker vis-à-vis a machine respectively circuit. This becomes important when such a set of properties is intended to play the role of a specification. Therefore, the invention is able to provide a necessary condition for the quality of a specification. This condition is not sufficient: There are sets of properties, which can be designated as being complete, although no circuit is present, which fulfill all the properties of such a property set.
For the purpose of control, the invention delivers a measure of completeness on a preferred basis, which allows the progress of the verification to be presented during the course of the project. This measurement increases in correlation to a growing number of properties and only returns the value 1 once the number of properties is complete. By means of this, the verification can be monitored much more precisely using a property checker than with all other procedures known to present.
Additional advantages and features of the invention and a detailed understanding can be obtained from the following description of the current execution forms preferred at this point in time, whereupon the description is intended to be purely illustrative and should not be regarded as being of a limiting nature. In this description, reference will be made to the attached diagrams, for which the following applies: